COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	cs258[w84,jmc]		List of lectures
C00003 00003	Miscellaneous
C00004 00004	sublis[pat,alist] ← if at pat
C00006 00005	I have a few new proof files in [prf,jk]:
C00009 ENDMK
C⊗;
cs258[w84,jmc]		List of lectures

Boyer and Moore theorem prover
(2 lectures)

Carolyn thesis (4)

blobs (1)

graphs (1)

Scottery (2)

Lambda calculus (1)

Floyd and Manna methods (2)

subgoal induction 1

data spaces 1

dynamic logic?, Hoare axioms?,

proofs about Prolog programs?

more on EKL 2

call by name, call-by-need, call-by-value

Goad 2

Manna or Waldinger ? 1

Jim Morris ?

C(F)
cs258[w82,jmc]		topics for cs258 for winter 1982
PROBLE.258[W79,JMC]	CS258←PROBLEM SET→WINTER 1979
NOTES.258[W79,JMC]	non-termination of certain functions
Miscellaneous

lispax.lsp[prf,jk]

f(m,n) ← if m = 0 then 0 else f(m-1,f(m,n))
sublis[pat,alist] ← if at pat
		    then [if isvar pat
			  then {assoc[pat,alist}[λz. if n z
							then error[]
							else d z]
			  else pat]
		    else sublis[a pat,alist].sublis[d pat,alist]

match[pat,exp,alist] ← if alist = NO
		       then NO
		       else if at pat
		       then [if isvar pat
			     then {assoc[pat,alist]}
				  [λz.if n z
				      then [pat.exp].alist
				      else [if d z = exp
					    then alist
					    else NO]]
			      else [if pat = exp then alist else NO]]
			else if at exp then NO
			else match[d pat,d exp,match[a pat,a exp,alist]]

∀pat exp alist. match[pat,exp,alist] ≠ NO
		 ⊃ sublis[pat,match[pat,exp,alist]] = exp


(define sublis
	|∀pat alist.
	sublis(pat,alist) = if atom pat
		    then [if isvar pat
			  then {assoc[pat,alist}[λz. if n z
							then error[]
							else d z]
			  else pat]
		    else sublis[a pat,alist].sublis[d pat,alist]

I have a few new proof files in [prf,jk]:

Subst.lsp[prf,jk] does the definition and properties of subst
(the unification algorithm does require the pars arguments to appear last:
 this is the reason for reversing arguments to subst)
Flat.lsp[prf,jk] does the definition and properties of flatten
Mapcar.lsp[prf,jk] does the definition and properties of mapcar on multiple lists
Distin.lsp[prf,jk] does the predicate distinct(a,b,c,..)=a≠b∧a≠c∧b≠c∧... for
arbitrary number of arguments.

Der uses now high order unification.

A bug or a feature?
Unrestricted Skolemisation is equivalent to Axiom of Choice.
Thus, we can verify it:

(proof foo)
(trw |(∀x.∃y.A(x,y))⊃(∃f.∀x.A(x,f(x)))| (der))
(∀X.(∃Y.A(X,Y)))⊃(∃F.(∀X.A(X,F(X))))

In my opinion, unrestricted Skolemization with its consequent axiom
of choice is a feature not a bug from any practical point of view.